A Formally Verified Unicode 17.0 Text Processing Library in SPARK/Ada with C bindings. A complete implementation of the Unicode 17.0 text processing stack, written in SPARK/Ada (Ada 2022) and formally verified with GNATprove.
